Nuprl Lemma : sum_arith1
4,23
postcript
pdf
n
:
,
a
,
b
:
. sum(
a
+
b
i
|
i
<
n
)
2 =
n
(
a
+
a
+
b
(
n
-1))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
primrec(
n
;
b
;
c
)
,
b
,
A
,
Prop
,
b
,
,
i
=
j
,
P
Q
,
P
&
Q
,
P
Q
,
Unit
,
,
sum(
f
(
x
) |
x
<
k
)
,
i
j
,
False
,
A
B
Lemmas
ge
wf
,
nat
properties
,
nat
wf
,
eqtt
to
assert
,
eqff
to
assert
,
iff
transitivity
,
assert
of
bnot
,
not
functionality
wrt
iff
,
assert
of
eq
int
,
eq
int
wf
,
bool
wf
,
bnot
wf
,
not
wf
,
assert
wf
,
primrec
wf
,
int
seg
wf
origin